div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
↳ QTRS
↳ DependencyPairsProof
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
I(div(X, Y)) → DIV(Y, X)
DIV(div(X, Y), Z) → DIV(i(X), Z)
DIV(X, e) → I(X)
DIV(div(X, Y), Z) → I(X)
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
I(div(X, Y)) → DIV(Y, X)
DIV(div(X, Y), Z) → DIV(i(X), Z)
DIV(X, e) → I(X)
DIV(div(X, Y), Z) → I(X)
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(div(X, Y), Z) → DIV(Y, div(i(X), Z))
I(div(X, Y)) → DIV(Y, X)
DIV(div(X, Y), Z) → DIV(i(X), Z)
DIV(X, e) → I(X)
DIV(div(X, Y), Z) → I(X)
The value of delta used in the strict ordering is 5/4.
POL(i(x1)) = x_1
POL(div(x1, x2)) = 1 + x_1 + x_2
POL(e) = 4
POL(DIV(x1, x2)) = 4 + (4)x_1
POL(I(x1)) = 5/4 + (4)x_1
div(X, e) → i(X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))
i(div(X, Y)) → div(Y, X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))